6 POSITIVE LINEAR FORMS, POSITIVE HUBERT FORMS 351 remains to be shown that T- (U(s) - z) = U'(s) - (T* z\ and by the principle of extension of identities we may assume that z is of the form U(t) • x0. But then U(s) - (U(t) - x0) = U(st ) • x0 , and therefore T- (U(st) - x0) = U'(st) - x0 = £/'(•*) - (U'(t) • x0) = U'(s) - (T - z). This completes the proof. Furthermore, the prehilbert space H0 can be defined directly in terms of the formfxo, and even in terms of the Hilbert form gXQ. We have the following general proposition: (15.6.8) Let g be a positive Hilbert form on A. Then the set n of elements s e A such that g(s, s) = 0 is a left ideal of A, and is equal to the set ofs G A such that g(s, t) = 0 for all t e A. If n : A ->• A/n is the canonical linear mapping, then there exists a unique structure of prehilbert space on A/n such that = g(s, t)for all s,teA. The Cauchy-Schwarz inequality \g(s, f)\2 <£ g(s, s)g(t, t) (6.2.1) shows that n is the set of all s e A such that g(s, f) = 0 for all t e A. The relation (15.63) then proves that n is a left ideal in A. By virtue of the relation g(t, s) = g(s, t\ we have g(t, s) = 0 for s e n and t e A; it follows that if s — s' e n and t - t' e n (that is, if n(s) = n(s') and n(t) = n(t')) then #(5-, t) = g(s', t'\ because g(s, f) - g(s , t') = g(s, t - tf) + g(s - s', tf). Since g(s, t) depends only on n(s) and n(i), we may write g(s, i) = (71(5-) |TI(*)), and it is straight- forward to check that the function (x\y) so defined on (A/n) x (A/n) is a non-degenerate positive hermitian form. In the case where g = gxo , we have ^(s, s) = || U(s) - xQ\\2, hence n is the kernel of the linear mapping u : s\-+ U(s) - x0 of A onto H0 . The formula (15.6.5) shows that the bijective mapping S: A/n-+H0 induced by u is a prehilbert space isomorphism. This shows, as stated earlier, that the Hilbert space H is determined by gxo up to isomorphism. Further, the representation s\~- > U(s) can be reconstructed from the algebra structure of A and the form gxo , because U(s) - (U(t) • *0) = U(s) ' (S • <0) = S ' n(st); and once U(s) is known in H0, it extends uniquely by continuity to H (5.5.4). Nevertheless, positive Hilbert forms of the type gxo are not the most general ones, for they satisfy an additional condition which expresses that eachespect to U